We give a purely model-theoretic characterization of the semantics of logicprograms with negation-as-failure allowed in clause bodies. In our semanticsthe meaning of a program is, as in the classical case, the unique minimum modelin a program-independent ordering. We use an expanded truth domain that has anuncountable linearly ordered set of truth values between False (the minimumelement) and True (the maximum), with a Zero element in the middle. The truthvalues below Zero are ordered like the countable ordinals. The values aboveZero have exactly the reverse order. Negation is interpreted as reflectionabout Zero followed by a step towards Zero; the only truth value that remainsunaffected by negation is Zero. We show that every program has a unique minimummodel M_P, and that this model can be constructed with a T_P iteration whichproceeds through the countable ordinals. Furthermore, we demonstrate that M_Pcan also be obtained through a model intersection construction whichgeneralizes the well-known model intersection theorem for classical logicprogramming. Finally, we show that by collapsing the true and false values ofthe infinite-valued model M_P to (the classical) True and False, we obtain athree-valued model identical to the well-founded one.
展开▼
